b:, x, y:Top. null(if b x else y fi) ~ if b null(x) else null(y) fi 

latex

Definitions	t  T, x:A. B(x), b, A, b, , Prop, P  Q, P & Q, P  Q, Unit, Top
Lemmas	top wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, bnot wf, not wf, assert wf